Nuprl Lemma : subtype_rel-equal
11,40
postcript
pdf
A
,
B
:Type. (
A
=
B
)
(
A
r
B
)
latex
ProofTree
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
t
T
,
Lemmas
subtype
rel
wf
origin
A, B:Type. (A = B) 
(A 
r B)
A, B:Type. (A = B) (A r B)
x:A. B(x) Q
T